COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	AXIOM ADHOC:
C00003 ENDMK
C⊗;
AXIOM ADHOC:
		∀N N1.(N ≥ SUCC N1 ⊃ N ≥ N1),
		∀N N1.(N ≥ SUCC N1 ⊃ ¬(N-N1=0)),
		∀N.(N-N=0),
		∀N.(N≥N),
		∀N.¬(N ≥ SUCC N);;